es:ES{i}, A:Type{i}, X:AbsInterface(A). es-interface-local{i:l}(es; A; X)  {i'} 

latex

Definitions

valtype(e), kindtype(i;k), t  T, val(e), state@i, state@i|xs, (state when e), ES, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), E, let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , es-M(es), tt, locl(a), t.1, t.2, x.A(x), kind(e), loc(e), x:A. B(x), , X is local, AbsInterface(A)

Lemmas

es-valtype-kindtype, subtype rel self, es-valtype wf, es-state-subtype-partial-state, pi2 wf, es-loc wf, es-kind wf, es-partial-state wf, pi1 wf, es-state-when wf, es-kindtype wf, es-val wf, es-E wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf